/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.semantic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.ComprehensionExpr;
import alloy.ast.Decl;
import alloy.ast.Id;
import alloy.ast.Location;
import alloy.ast.Module;
import alloy.ast.ModuleInfo;
import alloy.ast.MultiplicityExpr;
import alloy.ast.QuantifiedFormula;
import alloy.ast.SigExpr;
import alloy.ast.Signature;
import alloy.ast.SumIntExpr;
import alloy.ast.VarCreator;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.semantic.ExprTypeCheckVisitor.TypeCheckException;
import alloy.type.UnionType;
import alloy.util.Dbg;
import alloy.util.Msg;

/**
 * A visitor that type checks fields of signatures.  
 */

public class FieldTypeChecker {

	/**
	 * to record the fields of each union type
	 * (used to check for illegal field names:
	 * two fields with the same names belonging to 
	 * intersecting union types).  This is a map
	 * from UnionType to a List of Variables
	 */
	private final Map _unionTypesToFields = new HashMap();

	/** 
	 * Prevents others from instantiating this class.
	 *
	 */
	private FieldTypeChecker() {
		
	}
	
	/**
	 * Typechecks the fields of all signatures in the specification.
	 * Also, make sure no two signatures with the intersecting types have any fields
	 * with the same name.
	 * @param sigs_ a list of all signatures in the spec.  This list is assumed
	 *              to be sorted so that no signature appears before a signature
	 *              it extends.
	 */
	public static void typecheckFields(List sigs_) {
		
		final FieldTypeChecker f = new FieldTypeChecker();
		
		/* iterate through the signatures in topological order */
		Iterator sigIter = sigs_.iterator();
		while (sigIter.hasNext()) {
			Signature sig = (Signature) sigIter.next();
			f.typecheckFieldsOfSig(sig);
		}
	}

	/**
	 * Typecheck the fields of a given signature.  Ensure that the signature has
	 * no fields with the same name as any previously encountered signature
	 * with the intersecting type
	 * @param signature_ the signature whose fields should be typechecked
	 */
	private void typecheckFieldsOfSig(Signature signature_) {

		// a list of the fields of the current sigType
		// only used when checking for duplicate fields
		List unionTypeFields = null;

		UnionType unionType = signature_.getUnionType();

		
			
		// get the current list of fields for the signature type,
		// or create a new list if none exists
		if (!_unionTypesToFields.containsKey(unionType)) {
		    _unionTypesToFields.put(unionType, new ArrayList());
		}
		unionTypeFields = (List) _unionTypesToFields.get(unionType);
		
		// create a temporary local scope for typechecking
		// a copy of the local scope, plus a binding for "this" to
		// the signature type
		LocalScope typecheckLocalScope = signature_.getLocalScope().copy();
		
		try {
			typecheckLocalScope.addMapping("this", unionType);
		} catch (AlreadyMappedException ame) {
			Dbg.fatal("should not reach here");
		}

		Set moduleInfos = new HashSet();

		// get the modulescope associated with the signature
		ModuleInfo sigModuleInfo =
			((Module)signature_.getParent().getParent()).getModuleInfo();
		moduleInfos.add(sigModuleInfo);

		// get the local scope associated with the signature
		LocalScope sigLocalScope = signature_.getLocalScope();

		// type check each of the fields in the declarations of current signature
		Iterator decls = signature_.getDecls().getDeclIter();
		//System.out.println(signature_);
		while (decls.hasNext()) {

		    

			Decl decl = (Decl) decls.next();
			
			//System.out.println(" Field info: " + decl);
			
			MultiplicityExpr multExpr = decl.getExpr();

			// make sure the expression contains no invocations
			Object invRet = decl.getExpr().applyReturnVisitor(new InvocationErrorVisitor());
			if (invRet == null) {
				continue;
			}

			// make sure any field references in multiplicity
			// expr refer to only fields of current signature
			// or super sig
			try {
			    multExpr.applyVisitor(new CheckFieldRefsVisitor(signature_));
			} catch (CheckFieldRefsVisitor.InvalidFieldRefException e) { 
			    continue; 
			}
			
			// transform the multiplicity expression so that
			// all references to a field f become this.f
			// unless f is flagged with the @ sign
			VariableExpr thisVar = new VariableExpr(new Variable(new Id(Location.UNKNOWN, "this")));
			thisVar.setType(unionType);
		        FieldRefExpandingVisitor expander = new FieldRefExpandingVisitor(thisVar,
											 sigModuleInfo);
			MultiplicityExpr desugared = (MultiplicityExpr) multExpr.applyReturnVisitor(expander);

			// type check the expanded expression using the local scope binding
			// "this" to the signature type
			try {
				desugared = (MultiplicityExpr) 
				    ExprTypeCheckVisitor.typecheckNode(desugared, sigModuleInfo,
								       typecheckLocalScope);
				// if the type of desugared is empty, signal an error
				if (desugared.getType().isEmpty()) {
				    Dbg.user(new Msg("An expression used to define the type of a field cannot have an empty type", multExpr));
				    continue;
				}

				decl.setExpr(desugared);

			} catch (TypeCheckException e) {
				continue;
			}
			
			UnionType declType = desugared.getType();
					       
			// add variables to field local scope of sig
			Iterator variables = decl.getVariables().getVariableIter();
			while (variables.hasNext()) {
				Variable variable = (Variable) variables.next();
				String var = variable.getId().nodeString();

				// check for duplicate fields
				if (isDuplicated(unionType, var)) {
				    Dbg.user(new Msg("Duplicate field for type " + unionType, variable));
				    continue;
				} else {
				    unionTypeFields.add(var);
				}
				
				try {
				    					
					// give var the type signature type -> declType
					UnionType type = unionType.product(declType);
					sigLocalScope.addMapping(var, type);
					
					//System.out.println("field " + var + " :  " + type);
					
					//Dbg.info(var + " bound to type " + type.toString());
				} catch (AlreadyMappedException ame) {
					// should not be reached since we already checked for duplicate type
					// parameters
					Dbg.user(new Msg("Duplicate field in signature", variable));
				}
			}
			//System.out.println(" Field info desugared: " + multExpr);
			//System.out.println(" Field info desugared type: " + multExpr.getType());
		}
	      
	}

    /** 
     * @return true if var is a field name associated with two distinct intersecting
     * union types.
     **/
    private boolean isDuplicated(UnionType type, String var) {
		
	Iterator iter = _unionTypesToFields.keySet().iterator();
	while (iter.hasNext()) {
	    UnionType current = (UnionType) iter.next();
	    if ((!type.intersect(current).isEmpty()) &&
		(((List) _unionTypesToFields.get(current)).contains(var)))
		return true;
	}
	
	return false;
	
    }
   
	/**
	 * Visitor which ensures that a given multiplicity expression of a field
	 * declaration only refers to fields of the enclosing signature or 
	 * supersigs.  
	 */
    private static class CheckFieldRefsVisitor extends ASTDepthFirstVisitor {

		/** enclosing Signature */
		private final Signature _enclosingSig;

		/** module scope for module of enclosing sig */
		private final ModuleInfo _moduleScope;

		/** Set of String names created by some enclosing var. creator */
		private Set _shadowedNames = new HashSet();

		public CheckFieldRefsVisitor(Signature enclosingSig_) {
			_enclosingSig = enclosingSig_;
			_moduleScope =
				((Module)enclosingSig_.getParent().getParent()).getModuleInfo();
		}

		/**
		 * Visit a variable expr.  Ensure that the expression does not refer
		 * to an invalid field.
		 * @exception InvalidFieldRefException if expression refers to invalid field
		 */
		public void visit(VariableExpr varExpr_) {
		    ////System.out.println("varExpr: " + varExpr_);
			String varString = varExpr_.nodeString();
			try {
				_checkFieldRef(varString);
			} catch (InvalidFieldRefException e) {
				Dbg.user(new Msg("Reference to field not in enclosing sig or supersig", varExpr_));
				throw e;
			}
		}

		
		
		/**
		 * Check if a String represents a field which should not be referenced.
		 */
		private void _checkFieldRef(String fieldString_) {
			if (!_shadowedNames.contains(fieldString_)) {
				// see if it's a field of some signature
				// if it's not, do nothing (error will
				// be reported during typechecking)
				try {
					Iterator sigsWithFieldIter = _moduleScope.getSigsForField(fieldString_).iterator();
					
					while (sigsWithFieldIter.hasNext()) {
					    if (_inheritsFrom(_enclosingSig, (Signature)sigsWithFieldIter.next())) 
						{ return; }
					}
										
					// if we reach this point, no signature containing
					// the field passed the above extends test, so
					// this is an error
					throw new InvalidFieldRefException();
				} catch (ModuleInfo.NoSigsException e) {}
			
			}
		}
		
		public static class InvalidFieldRefException extends RuntimeException {}
	
	/**
	 * @return List of Signatures that are either supersets of sig_.  We assume sig_
	 * is a subset
	 **/
	private static List _getParents(Signature sig_) {
	    List parents = new ArrayList();
	    Iterator iter = sig_.getSubsets().getSigExprIter();
	    ModuleInfo moduleInfo = ((Module)sig_.getParent().getParent()).getModuleInfo();
	    while (iter.hasNext()) {
		parents.add(moduleInfo.getSignature(((SigExpr) iter.next()).getSig(), ""));
	    }
	    return parents;
	}
	/**
	 * @return true if subSig_ inherits fields from superSig_, either through extension
	 * or subsetting; otherwise returns false.  We assume that subSig_ is a subset.
	 **/
	private static boolean _inheritsFrom(Signature subSig_, Signature superSig_) {

	    if (subSig_ == superSig_) { 
		
		return true;
	    
	    } else {
		ModuleInfo moduleInfo = ((Module)subSig_.getParent().getParent()).getModuleInfo();
		Iterator iter = null;

		if (subSig_.isSubset())
		    iter = subSig_.getSubsets().getSigExprIter();
		else
		    iter = subSig_.getExtends().getSigExprIter();

		while (iter.hasNext()) {
		    Signature parentOfSubSig = moduleInfo.getSignature(((SigExpr) iter.next()).getSig(), "");
		    if (_inheritsFrom(parentOfSubSig, superSig_))
			return true;
		}

		return false;
	    }
	    

	}
	/**
	 * @return true if subSig_ extends superSig_ or subSig_ == superSig_.  
	 * We assume that subSig_ is not a subset.
	 */
	private static boolean _extends(Signature subSig_, Signature superSig_) {
	    
	    if (superSig_.isSubset()) return false;
	    return (superSig_.isSubset() ? false : subSig_.getSigType().isSubtypeOf(superSig_.getSigType()));
	}

		/**
		 * Visit a var. creator.  Note the names created, so they will
		 * be recognized as shadowed in the future.
		 */
		private void _handleVarCreator(VarCreator varCreator_) {
			// save old set of shadowed names
			Set oldShadowedNames = new HashSet(_shadowedNames);
			Iterator declIter = varCreator_.getDecls().getDeclIter();
			while (declIter.hasNext()) {
				Decl decl = (Decl)declIter.next();
				// visit mult. expr
				decl.getExpr().applyVisitor(this);
				Iterator varIter = decl.getVariables().getVariableIter();
				while (varIter.hasNext()) {
					_shadowedNames.add(((Variable)varIter.next()).nodeString());
				}
			}
			// visit body
			varCreator_.getBody().applyVisitor(this);
                        _shadowedNames = oldShadowedNames;
		}
		
		public void visit(QuantifiedFormula quantForm_) {
			_handleVarCreator(quantForm_);
		}
		
		public void visit(ComprehensionExpr compExpr_) {
			_handleVarCreator(compExpr_);
		}
		
		public void visit(SumIntExpr sumIntExpr_) {
			_handleVarCreator(sumIntExpr_);
		}
	}

}
